/* Benchmarks for the PionterC verifier. */

// list visit

struct list 
{
  int data;
  struct list* next;
};

/*@ let list(l) = (l==null) ||
  @               ({{l}} && list(l->next))
  @ in  list(l)
  @ end
  @*/
int traverse(strcut list* l)
{
  struct list* p;
  int sum;
  
  p=null;
  sum = 0;
  
  p = l;
  
  while(p!=null) /*@{{p, l}} && list(l->next) */ 
  {
    sum = sum + p->data;
    p = p->next;
  }
  p = null;
  return sum;
}
/*@ true
  @*/
  